es:ES, e:E, l:IdLnk, tg:Id.
(e sends on l with tag tg)
 (e':E.
 (isrcv(e'))
  (sender(e') = e)
  (lnk(e') = l)
  (tag(e') = tg)
  es-first-from(es;e;l;tg) loc e' ) 

latex

Definitions

False, A, Y, t  ...$L, i  j , A  B, suptype(S; T), S  T, ||as||, x:A. B(x), L1  L2, x before y  l, i  j < k, {i..j}, e loc e' , P  Q, (e <loc e'), Top, tt, if b then t else f fi , null(as), b, {T}, SQType(T), hd(l), True, T, x. t(x), xL. P(x), IdLnk, , t  T, P & Q, A c B, es-first-from(es;e;l;tg), P  Q, x:A. B(x), (e sends on l with tag tg), SqStable(P), x(s), l-ordered(T;x,y.R(x;y);L), loc-ordered(es;L), P  Q, P  Q, tag(e), lnk(e), isrcv(e)

Lemmas

non neg length, length cons, length nil, select wf, int seg wf, length wf nat, increasing wf, length wf1, le wf, l before filter, cons before, es-locl wf, cons member, l member set2, es-causl wf, es-loc wf, subtype rel set, l before wf, top wf, subtype rel list, null wf3, filter wf, member null, l member set, Knd sq, assert-eq-id, member filter, decidable assert, isrcv wf, sq stable from decidable, tagof wf, eq id wf, es-kind wf, filter type, l member wf, es-receives wf, list-set-type2, lnk wf, event system wf, es-sends-on wf, es-isrcv wf, assert wf, es-sender wf, es-E wf, es-lnk wf, IdLnk wf, es-tag wf, Id wf, loc-ordered-es-receives, member-es-receives